Inference at * 1 
Iof proof for Lemma before-adjacent:



1. T : Type
2. T List
3. x : T
4. y : T
5. no_repeats(T;[])
6. adjacent(T;[];x;y)
7. z : T
8. z before y  []
  z before x  []  (z = x) 

latex

 by ((FLemma `adjacent-nil` [6]) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	x:A. B(x), P  Q, x:AB(x), False
Lemmas	adjacent-nil